High integrity software is software that must be trusted to work dependably in some critical function, and whose failure to do so may have catastrophic results, such as serious injury, loss of life or property, business failure or breach of security. Some examples include software used in safety systems of nuclear power plants, medical devices, electronic banking, air traffic control, automated manufacturing, and military systems. The importance of high quality, low defect software is apparent in such critical situations. However, high integrity software is also important in more mundane business areas where defective software is often the norm.
Formal verification is the process of checking whether a design satisfies some requirements or properties. In order to formally verify a design, it must first be converted into a more condensed, verifiable format. The design is specified as a set of interacting systems, each having a finite number of configurations or states. States and transition between states constitute finite state machines (FSMs). The entire system is a FSM that can be obtained by composing the FSMs associated with each component. The first step in verification consists of obtaining a complete FSM description of the system. Given a present state (or current configuration), the next state (or successive configuration) of a FSM can be written as a function of its present state and inputs (transition function or transition relation). Formal verification attempts to execute every possible computational path with every possible state value to prove every possible state is consistent.
Once a formal specification has been verified, a software implementation of the formal specification is verified against the formal specification. This is typically done via visual inspection of the software implementation together with the corresponding detailed or formal specification of the software program. The formal specification and the implementation may be in separate files, or implementation source code may be interspersed with formal specification annotations corresponding to the implementation source code. Mechanisms exist to extract the annotations and verify them, as illustrated below with respect to FIG. 1A. Mechanisms also exist to extract the implementation source code and create implementation executable code, as illustrated below with respect to FIG. 1B.
Turning now to FIG. 1A, a block diagram that illustrates verification of formal specification statements extracted from a program source file is presented. A source file 100 includes implementation source code interspersed with formal specification annotations. An extractor/syntax checker receives the source file 100 and extracts the formal specification annotations to create a formal specification file 110. A verifier 115 receives the formal specification file 110 and verifies the formal specification statements to create a results file 120 including results of the verification.
Turning now to FIG. 1B, a block diagram that illustrates compiling and linking implementation source code extracted from a program source file is presented. Like source file 100 of FIG. 1A, source file 150 of FIG. 1B includes implementation source code interspersed with formal specification annotations. A compiler/linker 155 receives the source file 150, compiles the implementation source code and links the resultant object code to create to create an executable file 160 containing implementation executable code. The compiler/linker typically treats the annotations as comments and thus ignores them.
Unfortunately, the processes illustrated by FIGS. 1A and 1B are disjoint; the formal verification process illustrated by FIG. 1A proceeds without regard to the implementation source code corresponding to the annotations, and the compilation and linking process illustrated by FIG. 1B proceeds without regard to the formal specification annotations. Thus, verification of the implementation source code requires a visual inspection of the source file to confirm that the implementation source code complies with the constraints imposed by the formal specification annotations.
A virtual machine is an abstract computing machine generated by a software application or sequence of instructions that is executed by a processor. The term “architecture-neutral” refers to programs, such as those written in the Java™ programming language, which can be executed by a virtual machine on a variety of computer platforms having a variety of different computer architectures. Thus, for example, a virtual machine implemented on a Windows™-based personal computer system will execute an application using the same set of instructions as a virtual machine implemented on a UNIX™-based computer system. The result of the platform-independent coding of a virtual machine's sequence of instructions is a stream of one or more bytecodes, many of which are, for example, one-byte-long numerical codes.
The Java™ programming language is an object-oriented programming language. In an object-oriented system, a “class” describes a collection of data and methods that operate on that data. Taken together, the data and methods describe the state of and behavior of an object. Use of the Java™ programming language has found many applications including, for example, those associated with Web browsers. The Java™ programming language is described in detail in Gosling, et al., “The Java™ Language Specification”, August 1996, Addison-Wesley Longman, Inc. Programs written in the Java™ language execute on a virtual machine.
A Java™ virtual machine (JVM) executes virtual machine code written in the Java™ programming language and satisfies the Java™ Virtual Machine Specification (Lindholm, et al., “The Java™ Virtual Machine Specification”, April 1999, Addison-Wesley Longman, Inc., Second Edition). A Jav™ virtual machine (JVM) is an abstract computer architecture that can be implemented in hardware or software. Either implementation is intended to be included in the following description of a VM. For the purposes of this disclosure, the term “processor” may be used to refer to a physical computer or a virtual machine.
FIG. 2 is a block diagram that illustrates a Java™ class file. Methods are described via a descriptor component, a code component and one or more exception ranges. The descriptor component identifies the method name, calling parameters and other information about the method. The code component contains the executable code of the method. Each exception range associates a range of program counter values to the address of an exception handler to invoke if an exception is raised while executing code within the exception range.
A Java™ virtual machine executes programs written in the Java™ programming language and is designed for use on desktop computers, which are relatively rich in memory. However, various devices have relatively limited architectures. Resource-constrained devices are generally considered to be those that are relatively restricted in memory and/or computing power or speed, as compared to typical desktop computers and the like. Other resource-constrained devices include, by way of example, smart cards, cellular telephones, boundary scan devices, field programmable devices, personal digital assistants (PDAs) and pagers and other miniature or small footprint devices.
Smart cards are typically made of plastic or metal and have an electronic chip that includes an embedded microprocessor or microcontroller to execute programs and memory to store programs and data. Such devices, which can be about the size of a credit card, typically have computer chips with 8-bit or 16-bit architectures. Additionally, these devices typically have limited memory capacity. For example, some smart cards have less than one kilobyte (1K) of random access memory (RAM) as well as limited read only memory (ROM), and/or non-volatile memory such as electrically erasable programmable read only memory (EEPROM).
It would be desirable to write programs that use the full implementation of the Java™ virtual machine for execution on resource-constrained devices such as smart cards. However, due to the limited architecture and memory of resource-constrained devices such as smart cards, the full Java™ virtual machine platform cannot be implemented on such devices. Accordingly, a separate Java Card™ (the smart card that supports the Java™ programming language) technology supports a subset of the Java™ programming language for resource-constrained devices. Java Card™ technology is described in Chen, Z. Java Card™ Technology for Smart Cards—Architecture and Programmer's Guide, Boston, Addison-Wesley, 2000.
What is needed is solution for deployment of high integrity software that simplifies program verification. A further need exists for such a solution that provides automated verification of a software program specification with a corresponding software program implementation. A further need exists for such a solution that simplifies program verification of software developed for resource constrained devices such as smart cards. Yet a further need exists for such a solution that simplifies program verification of software developed for a Java Card™ technology-enabled device.